#include "ic3.h"
#include <iostream>
using std::cout;
using std::endl;

extern void state2clause( const State s , unsigned ns , Clause & x , Minisat::Lit * lit );
extern void state2state( const State s , unsigned ns , Clause & x , Minisat::Lit * lit );
extern void state2nstate( const State s , unsigned ns , Clause & x , Minisat::Lit * lit );
extern void clause2nstate( const Clause & y , unsigned ns , Clause & x , Minisat::Lit * lit);
extern void nclause2clause( const Clause & y , Clause & x , Minisat::Lit * rev);
extern void print_clause( const Clause & c , unsigned ns );

MinisatIC3 * IC3::createSolver( unsigned k )
{
   assert( F.size() == _clauses.size() );

   MinisatIC3 * s = new MinisatIC3 ( Finit , *this );

   for( unsigned i = k ; i < F.size() ; ++ i )
   {
      unsigned sz = _clauses[i].size();
      for( unsigned j = 0 ; j < sz ; ++ j )
      {
         const Clause * c = clause( i , j );
         if( c != NULL )
            s->addClause( *c );
      }
   }
   return s;
}

bool IC3::check_sat( unsigned i , State s )
{
   MinisatIC3 * f =  createSolver(i);
   Clause a(_nstates);
   state2state( s , _nstates , a , _lits );

   bool ret = f->solve(a);
   delete f;
   return ret;
}
bool IC3::isInductiveInvariant( unsigned i , const Clause & c )
{
   MinisatIC3 * F = createSolver( i );

   Clause a( c.size() ) , n( c.size() );
   bool ini = false;
   for( int i = 0 ; i < c.size() ; ++ i )
   {
      if( sign(c[i]) == true ) ini = true;
      n[i] = c[i];
      a[i] = _lits[ var(c[i]) + _nstates ] ^ sign( c[i] ) ^ 1;
   }
//   assert( ini );

   F->addClause( n );
   bool ret = F->solve( a );

   delete F;
   return ret == false;
}
bool IC3::check_ic3_A()
{
   assert( check_ic3_A1() );
   assert( check_ic3_A4() );
   return true;
}
bool IC3::check_ic3_A1()
{
   Clause c( _nstates );

   unsigned size = ((_nstates-1)>>6)+1;
   uint64_t * s0 = new uint64_t[ size ];

   memset( s0 , 0 , sizeof( uint64_t) * size );
   for( unsigned i = 1 ; i < F.size() ; ++i )
      assert( check_sat( i , s0 ) );
   return true;
}
bool IC3::check_ic3_Fi_imply_Fi_1( unsigned i )
{
   MinisatIC3 * f = F[i];
   if( f->solve( ~ _lits[_nstates<<1]) == true  ){
      cout << "ERROR state " << i << " Fi !=> P' " << endl;
      return false;
   }
   for( unsigned j = i+1 ; j < _clauses.size() ; ++ j )
   {
      unsigned sz = _clauses[j].size();
      for( unsigned k = 0 ; k < sz ; ++ k )
      {
         const Clause * c = clause( j , k );
         if( c==NULL )continue;
         Clause s( c->size() );
         clause2nstate( *c , _nstates , s , _lits );
         if( f->solve( s ) == true ){
            cout << "ERROR state "<< i << " Fi !=> c "<< endl;
            print_clause( *c , _nstates);
            return false;
         }
      }
   }
   return true;
}
bool IC3::check_ic3_A4()
{
   assert( F.size() == _clauses.size() );

   for( unsigned i = 0 ; i < F.size()-1 ; ++i ) 
      if( check_ic3_Fi_imply_Fi_1(i) == false )
      {
         assert( false );
         return false;
      }
   return true;
}
bool IC3::my_check( )
{
   for( unsigned i = 0 ; i < F.size() -1 ; ++ i )
   {
      if(  check_ic3_Fi_imply_Fi_1(i) == false)
      {
         assert( false);
         return false;
      }
   }
   return true;
}
/*bool MinisatIC3::isInductiveInvariant( const Clause & in )
{
   Clause c( in.size() ); 
   Clause a( in.size() );
   in.copyTo( c );
   clause2nstate( c , _nstates , a , _lits );

   Minisat::Lit ctrl = get_ctrl();
   c.push( ctrl );
   a.push( ~ctrl );
   addClause( c );
   bool ret = solve( a );
   addClause( ctrl );

   return ret == false;
}*/
